Termination w.r.t. Q proof of /home/nowonder/forschung/aprove/satrung/aprove/lpar3/TRCSRSLASHExAppendixB_AEL03

Termination w.r.t. Q of the following Term Rewriting System could not be shown:

Q restricted rewrite system:
The TRS R consists of the following rules:

a__from₁(X) -> cons₂(mark₁(X), from₁(s₁(X)))
a__2ndspos₂(0, Z) -> rnil
a__2ndspos₂(s₁(N), cons₂(X, Z)) -> a__2ndspos₂(s₁(mark₁(N)), cons2₂(X, mark₁(Z)))
a__2ndspos₂(s₁(N), cons2₂(X, cons₂(Y, Z))) -> rcons₂(posrecip₁(mark₁(Y)), a__2ndsneg₂(mark₁(N), mark₁(Z)))
a__2ndsneg₂(0, Z) -> rnil
a__2ndsneg₂(s₁(N), cons₂(X, Z)) -> a__2ndsneg₂(s₁(mark₁(N)), cons2₂(X, mark₁(Z)))
a__2ndsneg₂(s₁(N), cons2₂(X, cons₂(Y, Z))) -> rcons₂(negrecip₁(mark₁(Y)), a__2ndspos₂(mark₁(N), mark₁(Z)))
a__pi₁(X) -> a__2ndspos₂(mark₁(X), a__from₁(0))
a__plus₂(0, Y) -> mark₁(Y)
a__plus₂(s₁(X), Y) -> s₁(a__plus₂(mark₁(X), mark₁(Y)))
a__times₂(0, Y) -> 0
a__times₂(s₁(X), Y) -> a__plus₂(mark₁(Y), a__times₂(mark₁(X), mark₁(Y)))
a__square₁(X) -> a__times₂(mark₁(X), mark₁(X))
mark₁(from₁(X)) -> a__from₁(mark₁(X))
mark₁(2ndspos₂(X1, X2)) -> a__2ndspos₂(mark₁(X1), mark₁(X2))
mark₁(2ndsneg₂(X1, X2)) -> a__2ndsneg₂(mark₁(X1), mark₁(X2))
mark₁(pi₁(X)) -> a__pi₁(mark₁(X))
mark₁(plus₂(X1, X2)) -> a__plus₂(mark₁(X1), mark₁(X2))
mark₁(times₂(X1, X2)) -> a__times₂(mark₁(X1), mark₁(X2))
mark₁(square₁(X)) -> a__square₁(mark₁(X))
mark₁(0) -> 0
mark₁(s₁(X)) -> s₁(mark₁(X))
mark₁(posrecip₁(X)) -> posrecip₁(mark₁(X))
mark₁(negrecip₁(X)) -> negrecip₁(mark₁(X))
mark₁(nil) -> nil
mark₁(cons₂(X1, X2)) -> cons₂(mark₁(X1), X2)
mark₁(cons2₂(X1, X2)) -> cons2₂(X1, mark₁(X2))
mark₁(rnil) -> rnil
mark₁(rcons₂(X1, X2)) -> rcons₂(mark₁(X1), mark₁(X2))
a__from₁(X) -> from₁(X)
a__2ndspos₂(X1, X2) -> 2ndspos₂(X1, X2)
a__2ndsneg₂(X1, X2) -> 2ndsneg₂(X1, X2)
a__pi₁(X) -> pi₁(X)
a__plus₂(X1, X2) -> plus₂(X1, X2)
a__times₂(X1, X2) -> times₂(X1, X2)
a__square₁(X) -> square₁(X)

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

Q restricted rewrite system:
The TRS R consists of the following rules:

a__from₁(X) -> cons₂(mark₁(X), from₁(s₁(X)))
a__2ndspos₂(0, Z) -> rnil
a__2ndspos₂(s₁(N), cons₂(X, Z)) -> a__2ndspos₂(s₁(mark₁(N)), cons2₂(X, mark₁(Z)))
a__2ndspos₂(s₁(N), cons2₂(X, cons₂(Y, Z))) -> rcons₂(posrecip₁(mark₁(Y)), a__2ndsneg₂(mark₁(N), mark₁(Z)))
a__2ndsneg₂(0, Z) -> rnil
a__2ndsneg₂(s₁(N), cons₂(X, Z)) -> a__2ndsneg₂(s₁(mark₁(N)), cons2₂(X, mark₁(Z)))
a__2ndsneg₂(s₁(N), cons2₂(X, cons₂(Y, Z))) -> rcons₂(negrecip₁(mark₁(Y)), a__2ndspos₂(mark₁(N), mark₁(Z)))
a__pi₁(X) -> a__2ndspos₂(mark₁(X), a__from₁(0))
a__plus₂(0, Y) -> mark₁(Y)
a__plus₂(s₁(X), Y) -> s₁(a__plus₂(mark₁(X), mark₁(Y)))
a__times₂(0, Y) -> 0
a__times₂(s₁(X), Y) -> a__plus₂(mark₁(Y), a__times₂(mark₁(X), mark₁(Y)))
a__square₁(X) -> a__times₂(mark₁(X), mark₁(X))
mark₁(from₁(X)) -> a__from₁(mark₁(X))
mark₁(2ndspos₂(X1, X2)) -> a__2ndspos₂(mark₁(X1), mark₁(X2))
mark₁(2ndsneg₂(X1, X2)) -> a__2ndsneg₂(mark₁(X1), mark₁(X2))
mark₁(pi₁(X)) -> a__pi₁(mark₁(X))
mark₁(plus₂(X1, X2)) -> a__plus₂(mark₁(X1), mark₁(X2))
mark₁(times₂(X1, X2)) -> a__times₂(mark₁(X1), mark₁(X2))
mark₁(square₁(X)) -> a__square₁(mark₁(X))
mark₁(0) -> 0
mark₁(s₁(X)) -> s₁(mark₁(X))
mark₁(posrecip₁(X)) -> posrecip₁(mark₁(X))
mark₁(negrecip₁(X)) -> negrecip₁(mark₁(X))
mark₁(nil) -> nil
mark₁(cons₂(X1, X2)) -> cons₂(mark₁(X1), X2)
mark₁(cons2₂(X1, X2)) -> cons2₂(X1, mark₁(X2))
mark₁(rnil) -> rnil
mark₁(rcons₂(X1, X2)) -> rcons₂(mark₁(X1), mark₁(X2))
a__from₁(X) -> from₁(X)
a__2ndspos₂(X1, X2) -> 2ndspos₂(X1, X2)
a__2ndsneg₂(X1, X2) -> 2ndsneg₂(X1, X2)
a__pi₁(X) -> pi₁(X)
a__plus₂(X1, X2) -> plus₂(X1, X2)
a__times₂(X1, X2) -> times₂(X1, X2)
a__square₁(X) -> square₁(X)

Q is empty.

Q DP problem:
The TRS P consists of the following rules:

MARK₁(2ndspos₂(X1, X2)) -> MARK₁(X1)
A__2NDSNEG₂(s₁(N), cons2₂(X, cons₂(Y, Z))) -> A__2NDSPOS₂(mark₁(N), mark₁(Z))
A__2NDSPOS₂(s₁(N), cons2₂(X, cons₂(Y, Z))) -> A__2NDSNEG₂(mark₁(N), mark₁(Z))
A__PI₁(X) -> A__2NDSPOS₂(mark₁(X), a__from₁(0))
MARK₁(plus₂(X1, X2)) -> MARK₁(X2)
A__TIMES₂(s₁(X), Y) -> A__TIMES₂(mark₁(X), mark₁(Y))
MARK₁(negrecip₁(X)) -> MARK₁(X)
MARK₁(rcons₂(X1, X2)) -> MARK₁(X1)
A__TIMES₂(s₁(X), Y) -> MARK₁(X)
MARK₁(times₂(X1, X2)) -> MARK₁(X2)
A__2NDSNEG₂(s₁(N), cons₂(X, Z)) -> A__2NDSNEG₂(s₁(mark₁(N)), cons2₂(X, mark₁(Z)))
A__2NDSPOS₂(s₁(N), cons2₂(X, cons₂(Y, Z))) -> MARK₁(N)
MARK₁(plus₂(X1, X2)) -> A__PLUS₂(mark₁(X1), mark₁(X2))
A__2NDSPOS₂(s₁(N), cons₂(X, Z)) -> A__2NDSPOS₂(s₁(mark₁(N)), cons2₂(X, mark₁(Z)))
MARK₁(posrecip₁(X)) -> MARK₁(X)
MARK₁(times₂(X1, X2)) -> A__TIMES₂(mark₁(X1), mark₁(X2))
A__PI₁(X) -> MARK₁(X)
A__2NDSPOS₂(s₁(N), cons₂(X, Z)) -> MARK₁(Z)
MARK₁(s₁(X)) -> MARK₁(X)
MARK₁(rcons₂(X1, X2)) -> MARK₁(X2)
MARK₁(2ndspos₂(X1, X2)) -> A__2NDSPOS₂(mark₁(X1), mark₁(X2))
MARK₁(2ndsneg₂(X1, X2)) -> A__2NDSNEG₂(mark₁(X1), mark₁(X2))
A__2NDSPOS₂(s₁(N), cons₂(X, Z)) -> MARK₁(N)
MARK₁(pi₁(X)) -> MARK₁(X)
A__2NDSNEG₂(s₁(N), cons2₂(X, cons₂(Y, Z))) -> MARK₁(N)
A__SQUARE₁(X) -> MARK₁(X)
A__FROM₁(X) -> MARK₁(X)
MARK₁(plus₂(X1, X2)) -> MARK₁(X1)
A__2NDSNEG₂(s₁(N), cons2₂(X, cons₂(Y, Z))) -> MARK₁(Y)
A__TIMES₂(s₁(X), Y) -> A__PLUS₂(mark₁(Y), a__times₂(mark₁(X), mark₁(Y)))
MARK₁(times₂(X1, X2)) -> MARK₁(X1)
A__2NDSNEG₂(s₁(N), cons₂(X, Z)) -> MARK₁(N)
A__2NDSNEG₂(s₁(N), cons₂(X, Z)) -> MARK₁(Z)
MARK₁(cons2₂(X1, X2)) -> MARK₁(X2)
A__2NDSPOS₂(s₁(N), cons2₂(X, cons₂(Y, Z))) -> MARK₁(Z)
A__PLUS₂(s₁(X), Y) -> A__PLUS₂(mark₁(X), mark₁(Y))
MARK₁(from₁(X)) -> MARK₁(X)
A__PI₁(X) -> A__FROM₁(0)
MARK₁(from₁(X)) -> A__FROM₁(mark₁(X))
MARK₁(pi₁(X)) -> A__PI₁(mark₁(X))
MARK₁(cons₂(X1, X2)) -> MARK₁(X1)
A__SQUARE₁(X) -> A__TIMES₂(mark₁(X), mark₁(X))
A__PLUS₂(0, Y) -> MARK₁(Y)
MARK₁(2ndspos₂(X1, X2)) -> MARK₁(X2)
A__PLUS₂(s₁(X), Y) -> MARK₁(X)
MARK₁(square₁(X)) -> MARK₁(X)
MARK₁(2ndsneg₂(X1, X2)) -> MARK₁(X1)
MARK₁(square₁(X)) -> A__SQUARE₁(mark₁(X))
A__PLUS₂(s₁(X), Y) -> MARK₁(Y)
MARK₁(2ndsneg₂(X1, X2)) -> MARK₁(X2)
A__2NDSPOS₂(s₁(N), cons2₂(X, cons₂(Y, Z))) -> MARK₁(Y)
A__2NDSNEG₂(s₁(N), cons2₂(X, cons₂(Y, Z))) -> MARK₁(Z)
A__TIMES₂(s₁(X), Y) -> MARK₁(Y)

The TRS R consists of the following rules:

a__from₁(X) -> cons₂(mark₁(X), from₁(s₁(X)))
a__2ndspos₂(0, Z) -> rnil
a__2ndspos₂(s₁(N), cons₂(X, Z)) -> a__2ndspos₂(s₁(mark₁(N)), cons2₂(X, mark₁(Z)))
a__2ndspos₂(s₁(N), cons2₂(X, cons₂(Y, Z))) -> rcons₂(posrecip₁(mark₁(Y)), a__2ndsneg₂(mark₁(N), mark₁(Z)))
a__2ndsneg₂(0, Z) -> rnil
a__2ndsneg₂(s₁(N), cons₂(X, Z)) -> a__2ndsneg₂(s₁(mark₁(N)), cons2₂(X, mark₁(Z)))
a__2ndsneg₂(s₁(N), cons2₂(X, cons₂(Y, Z))) -> rcons₂(negrecip₁(mark₁(Y)), a__2ndspos₂(mark₁(N), mark₁(Z)))
a__pi₁(X) -> a__2ndspos₂(mark₁(X), a__from₁(0))
a__plus₂(0, Y) -> mark₁(Y)
a__plus₂(s₁(X), Y) -> s₁(a__plus₂(mark₁(X), mark₁(Y)))
a__times₂(0, Y) -> 0
a__times₂(s₁(X), Y) -> a__plus₂(mark₁(Y), a__times₂(mark₁(X), mark₁(Y)))
a__square₁(X) -> a__times₂(mark₁(X), mark₁(X))
mark₁(from₁(X)) -> a__from₁(mark₁(X))
mark₁(2ndspos₂(X1, X2)) -> a__2ndspos₂(mark₁(X1), mark₁(X2))
mark₁(2ndsneg₂(X1, X2)) -> a__2ndsneg₂(mark₁(X1), mark₁(X2))
mark₁(pi₁(X)) -> a__pi₁(mark₁(X))
mark₁(plus₂(X1, X2)) -> a__plus₂(mark₁(X1), mark₁(X2))
mark₁(times₂(X1, X2)) -> a__times₂(mark₁(X1), mark₁(X2))
mark₁(square₁(X)) -> a__square₁(mark₁(X))
mark₁(0) -> 0
mark₁(s₁(X)) -> s₁(mark₁(X))
mark₁(posrecip₁(X)) -> posrecip₁(mark₁(X))
mark₁(negrecip₁(X)) -> negrecip₁(mark₁(X))
mark₁(nil) -> nil
mark₁(cons₂(X1, X2)) -> cons₂(mark₁(X1), X2)
mark₁(cons2₂(X1, X2)) -> cons2₂(X1, mark₁(X2))
mark₁(rnil) -> rnil
mark₁(rcons₂(X1, X2)) -> rcons₂(mark₁(X1), mark₁(X2))
a__from₁(X) -> from₁(X)
a__2ndspos₂(X1, X2) -> 2ndspos₂(X1, X2)
a__2ndsneg₂(X1, X2) -> 2ndsneg₂(X1, X2)
a__pi₁(X) -> pi₁(X)
a__plus₂(X1, X2) -> plus₂(X1, X2)
a__times₂(X1, X2) -> times₂(X1, X2)
a__square₁(X) -> square₁(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

MARK₁(2ndspos₂(X1, X2)) -> MARK₁(X1)
A__2NDSNEG₂(s₁(N), cons2₂(X, cons₂(Y, Z))) -> A__2NDSPOS₂(mark₁(N), mark₁(Z))
A__2NDSPOS₂(s₁(N), cons2₂(X, cons₂(Y, Z))) -> A__2NDSNEG₂(mark₁(N), mark₁(Z))
A__PI₁(X) -> A__2NDSPOS₂(mark₁(X), a__from₁(0))
MARK₁(plus₂(X1, X2)) -> MARK₁(X2)
A__TIMES₂(s₁(X), Y) -> A__TIMES₂(mark₁(X), mark₁(Y))
MARK₁(negrecip₁(X)) -> MARK₁(X)
MARK₁(rcons₂(X1, X2)) -> MARK₁(X1)
A__TIMES₂(s₁(X), Y) -> MARK₁(X)
MARK₁(times₂(X1, X2)) -> MARK₁(X2)
A__2NDSNEG₂(s₁(N), cons₂(X, Z)) -> A__2NDSNEG₂(s₁(mark₁(N)), cons2₂(X, mark₁(Z)))
A__2NDSPOS₂(s₁(N), cons2₂(X, cons₂(Y, Z))) -> MARK₁(N)
MARK₁(plus₂(X1, X2)) -> A__PLUS₂(mark₁(X1), mark₁(X2))
A__2NDSPOS₂(s₁(N), cons₂(X, Z)) -> A__2NDSPOS₂(s₁(mark₁(N)), cons2₂(X, mark₁(Z)))
MARK₁(posrecip₁(X)) -> MARK₁(X)
MARK₁(times₂(X1, X2)) -> A__TIMES₂(mark₁(X1), mark₁(X2))
A__PI₁(X) -> MARK₁(X)
A__2NDSPOS₂(s₁(N), cons₂(X, Z)) -> MARK₁(Z)
MARK₁(s₁(X)) -> MARK₁(X)
MARK₁(rcons₂(X1, X2)) -> MARK₁(X2)
MARK₁(2ndspos₂(X1, X2)) -> A__2NDSPOS₂(mark₁(X1), mark₁(X2))
MARK₁(2ndsneg₂(X1, X2)) -> A__2NDSNEG₂(mark₁(X1), mark₁(X2))
A__2NDSPOS₂(s₁(N), cons₂(X, Z)) -> MARK₁(N)
MARK₁(pi₁(X)) -> MARK₁(X)
A__2NDSNEG₂(s₁(N), cons2₂(X, cons₂(Y, Z))) -> MARK₁(N)
A__SQUARE₁(X) -> MARK₁(X)
A__FROM₁(X) -> MARK₁(X)
MARK₁(plus₂(X1, X2)) -> MARK₁(X1)
A__2NDSNEG₂(s₁(N), cons2₂(X, cons₂(Y, Z))) -> MARK₁(Y)
A__TIMES₂(s₁(X), Y) -> A__PLUS₂(mark₁(Y), a__times₂(mark₁(X), mark₁(Y)))
MARK₁(times₂(X1, X2)) -> MARK₁(X1)
A__2NDSNEG₂(s₁(N), cons₂(X, Z)) -> MARK₁(N)
A__2NDSNEG₂(s₁(N), cons₂(X, Z)) -> MARK₁(Z)
MARK₁(cons2₂(X1, X2)) -> MARK₁(X2)
A__2NDSPOS₂(s₁(N), cons2₂(X, cons₂(Y, Z))) -> MARK₁(Z)
A__PLUS₂(s₁(X), Y) -> A__PLUS₂(mark₁(X), mark₁(Y))
MARK₁(from₁(X)) -> MARK₁(X)
A__PI₁(X) -> A__FROM₁(0)
MARK₁(from₁(X)) -> A__FROM₁(mark₁(X))
MARK₁(pi₁(X)) -> A__PI₁(mark₁(X))
MARK₁(cons₂(X1, X2)) -> MARK₁(X1)
A__SQUARE₁(X) -> A__TIMES₂(mark₁(X), mark₁(X))
A__PLUS₂(0, Y) -> MARK₁(Y)
MARK₁(2ndspos₂(X1, X2)) -> MARK₁(X2)
A__PLUS₂(s₁(X), Y) -> MARK₁(X)
MARK₁(square₁(X)) -> MARK₁(X)
MARK₁(2ndsneg₂(X1, X2)) -> MARK₁(X1)
MARK₁(square₁(X)) -> A__SQUARE₁(mark₁(X))
A__PLUS₂(s₁(X), Y) -> MARK₁(Y)
MARK₁(2ndsneg₂(X1, X2)) -> MARK₁(X2)
A__2NDSPOS₂(s₁(N), cons2₂(X, cons₂(Y, Z))) -> MARK₁(Y)
A__2NDSNEG₂(s₁(N), cons2₂(X, cons₂(Y, Z))) -> MARK₁(Z)
A__TIMES₂(s₁(X), Y) -> MARK₁(Y)

The TRS R consists of the following rules:

a__from₁(X) -> cons₂(mark₁(X), from₁(s₁(X)))
a__2ndspos₂(0, Z) -> rnil
a__2ndspos₂(s₁(N), cons₂(X, Z)) -> a__2ndspos₂(s₁(mark₁(N)), cons2₂(X, mark₁(Z)))
a__2ndspos₂(s₁(N), cons2₂(X, cons₂(Y, Z))) -> rcons₂(posrecip₁(mark₁(Y)), a__2ndsneg₂(mark₁(N), mark₁(Z)))
a__2ndsneg₂(0, Z) -> rnil
a__2ndsneg₂(s₁(N), cons₂(X, Z)) -> a__2ndsneg₂(s₁(mark₁(N)), cons2₂(X, mark₁(Z)))
a__2ndsneg₂(s₁(N), cons2₂(X, cons₂(Y, Z))) -> rcons₂(negrecip₁(mark₁(Y)), a__2ndspos₂(mark₁(N), mark₁(Z)))
a__pi₁(X) -> a__2ndspos₂(mark₁(X), a__from₁(0))
a__plus₂(0, Y) -> mark₁(Y)
a__plus₂(s₁(X), Y) -> s₁(a__plus₂(mark₁(X), mark₁(Y)))
a__times₂(0, Y) -> 0
a__times₂(s₁(X), Y) -> a__plus₂(mark₁(Y), a__times₂(mark₁(X), mark₁(Y)))
a__square₁(X) -> a__times₂(mark₁(X), mark₁(X))
mark₁(from₁(X)) -> a__from₁(mark₁(X))
mark₁(2ndspos₂(X1, X2)) -> a__2ndspos₂(mark₁(X1), mark₁(X2))
mark₁(2ndsneg₂(X1, X2)) -> a__2ndsneg₂(mark₁(X1), mark₁(X2))
mark₁(pi₁(X)) -> a__pi₁(mark₁(X))
mark₁(plus₂(X1, X2)) -> a__plus₂(mark₁(X1), mark₁(X2))
mark₁(times₂(X1, X2)) -> a__times₂(mark₁(X1), mark₁(X2))
mark₁(square₁(X)) -> a__square₁(mark₁(X))
mark₁(0) -> 0
mark₁(s₁(X)) -> s₁(mark₁(X))
mark₁(posrecip₁(X)) -> posrecip₁(mark₁(X))
mark₁(negrecip₁(X)) -> negrecip₁(mark₁(X))
mark₁(nil) -> nil
mark₁(cons₂(X1, X2)) -> cons₂(mark₁(X1), X2)
mark₁(cons2₂(X1, X2)) -> cons2₂(X1, mark₁(X2))
mark₁(rnil) -> rnil
mark₁(rcons₂(X1, X2)) -> rcons₂(mark₁(X1), mark₁(X2))
a__from₁(X) -> from₁(X)
a__2ndspos₂(X1, X2) -> 2ndspos₂(X1, X2)
a__2ndsneg₂(X1, X2) -> 2ndsneg₂(X1, X2)
a__pi₁(X) -> pi₁(X)
a__plus₂(X1, X2) -> plus₂(X1, X2)
a__times₂(X1, X2) -> times₂(X1, X2)
a__square₁(X) -> square₁(X)

Q is empty.
We have to consider all minimal (P,Q,R)-chains.